D:Dsys, i:Id, k:Knd.
(l:IdLnk, tg:Id. M(source(l)).dout(l,tg)  M(destination(l)).din(l,tg))
 (d-decl(D;i)(k))  M(i).da(k) 

latex

Definitions	Void, M(i), M.da(a), x:A. B(x), t  T, destination(l), Id, s = t, Prop, b, Type, A, b, , M.dout(l,tg), a = b, x:AB(x), P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, locl(a), if b t else f fi, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, w-action-dec(TA;M;i), d-decl(D;i), Dsys, M.din(l,tg), source(l), IdLnk, f(a), rcv(l,tg)
Lemmas	rcv wf, IdLnk wf, ma-dout wf, lsrc wf, ma-din wf, Knd wf, dsys wf, subtype rel self, ma-da wf, d-m wf, locl wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, Id wf, ldst wf